e(e1,e2].P(e) == e:E. (e1 <loc e) & e  e2  & P(e) 

latex

---

clarification:

existse-between3(es;e1;e2;e.P(e)) == e:es-E(es). es-locl(es; e1; e) & es-le(es;e;e2) & P(e) 

latex

Definitions	x:A. B(x), E, A & B, P & Q, (e <loc e'), e  e'
FDL editor aliases	existse-between3